The advancement of network technologies such as bluetooth and WiFi has promoted the development of the Internet of Things(IoT). IoT facilitates people's lives, but there are also serious security issues in it. Without secure access control, illegal access of IoT may bring losses to users in many aspects. Traditional access control methods usually rely on a trusted central node, which is not suitable for an IoT environment with nodes distributed. The blockchain technology and smart contracts provide a more effective solution for access control in IoT applications. However, it is difficult to ensure the correctness of smart contracts used for access control in IoT applications by using general test methods. To solve this problem, a method was proposed to formally verify the correctness of smart contracts for access control by using model checking tool Verds. In the method, the state transition system was used to define the semantics of the Solidity smart contract, the Computation Tree Logic(CTL) formula was used to describe the properties to be verified, and the smart contract interaction and user behavior were modelled to form the input model of Verds and the properties to be verified. And then Verds was used to verify whether the properties to be verified are correct. The core of this method is the translation from a subset of Solidity to the input model of Verds. Experimental results on two smart contracts for access control of IoT source show that the proposed method can be used to verify some typical scenarios and expected properties of access control contracts, thereby improving the reliability of smart contracts.

Concerning the limitations of person safety and difficulties in nodes repair, placement, search and rescue caused by complex or unreachable special areas where the Wireless Sensor Network (WSN) deployed in, an autonomous mobile strategy of carrier in WSN was proposed. Firstly, the localization of the carrier with fewer anchor nodes was realized by combining the maximum likelihood method and Received Signal Strength Indication (RSSI). Then, relying on the mathematical model, carrier moved autonomously in WSN by acquiring current position information and target node coordinates to amend the direction angle and select the next target node. The simulation results show that the proposed strategy can ensure the carrier to reach the destination along the shorter path and in less time, and the higher the density of sensor nodes is, the more likely this strategy will succeed. The WSN with 130, 180 and 300 nodes were simulated respectively, and the success rate was as high as 96.7%.

Since the time consumption of full-result query for big data is excessively high, the system Probery was proposed. Different from traditional approximate query, Probery adopted an approximate full-result query method, an original method to query data. The approximation of Probery referred to the probability of containing all data satisfying query conditions in query results. Firstly, Probery divided the data stored in system into multiple data segments. Secondly, Probery placed the data in Distributed File System (DFS) according to the probability placing model. Finally, given a query condition, Probery adopted a heuristic query method to query data probably. The performance of query data was shown by comparing with other dominated non-relational data management system, in the case that the completeness of result set lost by 8%. The query time consumption of Probery was saved by 51% compared with HBase, by 23% compared with Cassandra, by 12% compared with MongoDB, by 3% compared with Hive. The experimental results show that Probery improves the performance of query data when the completeness of query data losses appropriately. In addition, Probery has better generality, adaptability and extensibility for big data query.